package systemfnomabss



object InterpreterTest {
  
  
    import scala.testing.SUnit._
    
    

    def main(args:Array[String])= {
      val tr = new TestResult
      new TestSuite(
        
        /*
        new test23_4_warmup,
        new testChurchNumerals,
        */
        new test24_1_warmup,
        /*
        new testTypeIntoTypeSubstitution,

         
        new testParseApp1,
        new testParseApp2,
        //new testParseApp3,
        new testParseLambdas,
        
        new testEx9_2_2_1,
        
        new testIdBool ,
        
        new testIdInt,
        new testIfThenElse,
        
        new testInvert,
        
        new test01kwi,
        
        new testNoSubRecord,
        
        new testNoSubRecordAndFun,
        
        new testBinding,
        
        new testChunkUnwrap
        */
        //new testLoopy
        
         
    ).run(tr)

      for(f <- tr.failures())   Console println f
    }
    

    val verbose=true
    val ipret = new systemfInterpreter(verbose)//new Interpreter(true) with TypedLambdaParser with SystemFTypeCheck with SystemFEvaluator

    import ipret._
    
    

    class test23_4_warmup extends TestCase("examples TAPL 23.4 universal"){
      
      override def runTest () = {
        println("================\n"+name+"\n")
      
      val codeid = "\\[] X . \\x:X . x"
      eval(codeid)
      
      val codeidInt = "(" + codeid + ")"+"[int]";
        {val n = Name("x")
      assertEquals(Lam(TyInt(),n\\Var(n)), eval(codeidInt)) }
      
      val codedouble = "\\[]X . \\f:(X=>X) . \\a:X . (f (f a))"
      eval(codedouble)
      
      val codedoubleint = "("+codedouble + ") [int]";
        { val f= Name("f"); val a= Name("a");
      assertEquals(Lam(TyArr(TyInt(),TyInt()),f\\ 
                      Lam(TyInt(),a\\ 
                          App(Var(f),App(Var(f),Var(a))))),
                   eval(codedoubleint)) }
                   

      
      val codedoubleInttoInt = "("+codedouble +") [ (int=>int)]"
      eval(codedoubleInttoInt)
      
      val codedoubleSelfApp = "\\x: forall X. (X=>X) . (x [ forall Y. (Y=>Y)] x)"
      eval(codedoubleSelfApp)
      
      val codequad = "let double = "+codedouble+" in \\[]Y. \\f:(Y=>Y).\\a:Y.(double [Y] (double[Y] f) a)"
      eval(codequad)
      eval("let double = "+codedouble+" in  (\\[]Y. \\f:(Y=>Y).\\a:Y.(double [Y] (double[Y] f) a))[bool] ")
      
      val codequadruple = "let double = "+codedouble+" in \\[]Y. (double [ (Y=>Y)] (double [Y]))"
      eval(codequadruple)
      
      val codequadrupleBool = "let double = "+codedouble+" in ( (\\[]Y. (double [ (Y=>Y)] (double [Y]))) [bool])"
      eval(codequadrupleBool)
      
      
      }
      

    }
    class testChurchNumerals extends TestCase("applying of church numerals") {
      
      override def runTest() = {
        println("================\n"+name+"\n")
      
      
      val codeCNat = "forall X.((X=>X)=>(X=>X))"
      val codeS = "\\t:bool . if t then false else true"
      val codeZ = "true"
        
      val codec0 = "\\[] X . \\s:(X=>X) z:X . z"
      println("c0=");eval (codec0)
      val codec0app = "let S = "+codeS+" in let Z = "+codeZ+" in (("+codec0+") [bool] S) Z"
      assertEquals(Tru(),
                   eval(codec0app))
      
      val codec1 = "\\[] X . \\s:(X=>X) z:X . (s z)"
      println("c1=");eval (codec1)
      val codec1app = "let S = "+codeS+" in let Z = "+codeZ+" in (("+codec1+") [bool] S) Z"
      assertEquals(Fls(),
                   eval(codec1app))
      
      
      val codec2 = "\\[] X . \\s:(X=>X) z:X . (s (s z))"
      println("c2=");eval (codec2)
      val codec2app = "let S = "+codeS+ " in let Z = "+codeZ+" in (("+codec2+") [bool]  S )  Z"
      assertEquals(Tru(),
                   eval(codec2app))
      
      val codecsucc = "\\n:"+codeCNat+" . \\[]Y. \\s:(Y=>Y)  z:Y . ( s ( n [Y] s z))"
      println("csucc=");eval(codecsucc)
      val codecsuccapp ="let c0="+codec0+" in let ss = "+codeS+" in let zz = "+codeZ+" in ("+codecsucc+" c0) [bool] ss zz"
      assertEquals(Fls(),
                   eval(codecsuccapp))
    }
    }
    
    class test24_1_warmup extends TestCase("examples TAPL 24.1 existential") {
      override def runTest() = {
        println("================\n"+name+"\n")
      
      println("p2")
      val codep2 = "{* int, 0} as { forsome  X ,  X}"
      val X = Name("X")
      assertEquals(Pack(TyInt(),Lit(0),TyExist( X \\TyVar(X))),
                   eval(codep2))
      
      
      println("p3")
      val codep3 = "{* bool, true} as { forsome  X ,  X}"
      assertEquals(Pack(TyBool(),Tru(),TyExist( X \\TyVar(X))),
                   eval(codep3))
      
      println("p4")
      val codep4 = "{* int, { a=0, f=\\x:int . x}} as { forsome X, {a:X, f:(X=>int)}}"
      eval(codep4)
      
      println("p5")
      val codep5 = "{* bool, { a=true, f=\\x:bool . 0}} as { forsome X, {a:X, f:(X=>int)}}"
      eval(codep5)
      
      println("unpack1")
      val codeunpack1 = "import "+codep4+" into { X, x} in ( (from x fld f) (from x fld a) )"
      assertEquals(Lit(0),
                   eval(codeunpack1))
      
      println("unpack2")
      val codeunpack2 = "let p5 = "+codep5+" in import p5 into { X,x} in (x.f x.a)"
      assertEquals(Lit(0),
                   eval(codeunpack2))
      
      println("packbool")
      val codepackbool = "{* bool, { v=true, f=\\x:bool . if x then false else true }} as { forsome X, {v:X, f:(X=>bool)}}"
      eval(codepackbool)
      
      println("unpackbool")
      val codeunpackbool1 = "let pack = "+codepackbool+" in import pack into { B,b} in (b.f b.v) "
      assertEquals(Fls(),
                   eval(codeunpackbool1))
      
      /*
      println("unpackboolconcrete")
      val codeunpackboolconcrete = "let pack = "+codepackbool+" in import pack into { B,b} in ( (b.f [int]) b.v)) "
      eval(codeunpackboolconcrete)
      */

       //type variable is unknown, so ops on the real type are not allowed
       println("unpackboolleaky1")
      val codeunpackboolleaky1 = "let pack = "+codepackbool+" in import pack into {B,b} in (if b.v then true else false)"
      try { eval(codeunpackboolleaky1)
            //throw new Exception("leaky in existential unpackboolleaky1 not detected")
      } catch {
        case e:TypeExc => println("OK:"+e.getMessage)
      }

      //type variable leaves scope
      println("unpackboolleaky2")
      val codeunpackboolleaky2 = "let pack = "+codepackbool+" in import pack into { B,b} in (b.v) "
        try { eval(codeunpackboolleaky2)
              throw new Exception("leaky in existential unpackboolleaky2 not detected")
        } catch {
          case e:TypeExc => println("OK:"+e.getMessage)
        }
      
      }
    }
    
    
    
    class testTypeIntoTypeSubstitution extends TestCase("testTypeIntoTypeSubstitution") {
      override def runTest() = {
        println("================\n"+name+"\n")
        
        //object ops extends systemfdebruijnSubstitution with AbstractSyntax
        //import ops.*
       // assertEquals(TyVar(1),addingBinder(TyVar(0)))
       // assertEquals(TyVar(3),addingBinder(addingBinder(addingBinder(TyVar(0)))))
        //assertEquals(TyVar(1),ops.underBinder( ()=>TyVar(0)))
       //import DeBruijnOps._
       val x = Name("x");val y = Name("y"); val X=Name("X"); val Y=Name("Y")
       val codetermterm1 = "\\ x:int . x 42"
     
       val termterm1 = App(Lam(TyInt(),x\\Var(x)), Lit(42))
      assertEquals("code termterm 1",Lit(42),eval(codetermterm1))
      assertEquals("eval termterm 1",Lit(42),eval(termterm1))
      //assertEquals("raw  termterm 1",Lit(42),termSubstTop(Lit(42),Var(0)))
      //assertEquals("nice termterm 1",Lit(42),substituteterm(Lit(42)).asTop.intoterm(Var(0)))
      
      val codetermterm2 = "\\ x:int y:int. x 42"

      val termterm2 = App(Lam(TyInt(),x\\Lam(TyInt(), y\\Var(x))), Lit(42))
      assertTrue("code termterm 2", Lam(TyInt(),x\\Lit(42)) == (eval(codetermterm2)))
      assertEquals("eval termterm 2", Lam(TyInt(),y\\Lit(42)),eval(termterm2))
      //assertEquals("raw termterm 2 ", Lam("y",TyInt(),Lit(42)),
      //        termSubstTop(Lit(42),Lam("y",TyInt(), Var(1))))
      //assertEquals("nice termterm 2", Lam("y",TyInt(),Lit(42)),
      //    substituteterm(Lit(42)).asTop.intoterm(Lam("y",TyInt(), Var(1))))
      
      
      
      val codetypeterm1= "(\\[] X . \\x:X.x) [int]"
      val typeterm1 = TApp(TLam(X\\Lam(TyVar(X),x\\Var(x))), TyInt())
      assertEquals("code typeterm 1",Lam(TyInt(),x\\Var(x)),       eval(codetypeterm1))
      assertEquals(TyArr(TyInt(),TyInt()),                        typeOf(typeterm1))
      assertEquals("eval typeterm 1",Lam(TyInt(),x\\Var(x)),       eval(typeterm1))
      //assertEquals("raw  typeterm 1",Lam(TyInt(),x\\Var(x)),       typeintotermSubstTop(TyInt(),Lam("x",TyVar(0),Var(0))))
      assertEquals("nice typeterm 1",Lam(TyInt(),x\\Var(x)),       substitutetype(TyInt()).as(X).intoterm(Lam(TyVar(X),x\\Var(x))))
      
      val codetypeterm2="(\\[] X. \\[] Y. \\x:X.x) [int]"
      val typeterm2 = TApp(TLam(X\\TLam(Y\\Lam(TyVar(X),x\\Var(x)))), TyInt())
      assertEquals("code typeterm 2",TLam(Y\\Lam(TyInt(), x\\Var(x))),       eval(codetypeterm2))
      assertEquals(TyUniv(Y\\TyArr(TyInt(),TyInt())),                    typeOf(typeterm2))
      assertEquals("eval typeterm 2",TLam(Y\\Lam(TyInt(), x\\Var(x))),       eval(typeterm2))
      //assertEquals("raw  typeterm 2",TLam(Y\\Lam(TyInt(), x\\Var(x))),       typeintotermSubstTop(TyInt(),TLam("Y",Lam("x",TyVar(1),Var(0)))))
      assertEquals("nice typeterm 2",TLam(Y\\Lam(TyInt(), x\\Var(x))),       substitutetype(TyInt()).as(X).intoterm(TLam(Y\\Lam(TyVar(X),x\\Var(x)))))
      
      //as in "(\\[] X . \\x:X.x) [int]" when typing function
      val type1 = TyArr(TyVar(X),TyVar(X))
      //assertEquals(TyArr(TyInt(),TyInt()), typeintotypeSubstTop(TyInt(), TyArr(TyVar(0),TyVar(0))))   
      assertEquals(TyArr(TyInt(),TyInt()), substitutetype(TyInt()).as(X).intotype(TyArr(TyVar(X),TyVar(X))))   
      
      //as in "(\\[] X. \\[] Y. \\x:X.x) [int]"
      val type2 = TyUniv(Y\\TyArr(TyVar(X),TyVar(X)))
      assertEquals(TyUniv(Y\\TyArr(TyInt(),TyInt())), substitutetype(TyInt()).as(X).intotype(type2))
      //assertEquals(TyUniv(Y\\TyArr(TyInt(),TyInt())), typeintotypeSubstTop(TyInt(),type2))
      
       
      }}
    
      
    
    class testParseApp1 extends TestCase("testParseApp1"){
      override def runTest() ={
        println("================\n"+name+"\n")
       val code = "(unit unit) unit unit"
       val parsedAST = parseStringRaw(code) getOrElse exit
       assertEquals(RApp(RApp(RApp(RUnit(),RUnit()),RUnit()),RUnit()), 
                    parsedAST)
    }}
    
    class testParseApp2 extends TestCase("testParseApp2"){
     override def runTest() ={
       println("================\n"+name+"\n")
       val code ="s t u"
       val parsedAST = parseStringRaw(code) getOrElse exit
       assertEquals(RApp(RApp(RVarName("s"),RVarName("t")),RVarName("u")), 
           parsedAST)
    }}
    
    class testParseApp3 extends TestCase("testParseApp3"){
      override def runTest() ={
        println("================\n"+name+"\n")
      val code = " ((\\[] X. \\[] Y . true) [int]) [bool]"
      val parsedAST = parseString(code) getOrElse exit
      println(parsedAST)
      eval(code)
    }}
    
    class testParseLambdas  extends TestCase("testParseLambdas"){
      override def runTest() ={
        println("================\n"+name+"\n")
      val code = "\\x:bool. \\y:int . \\z:bool . z false 42 true"
      assertEquals(Tru(),
                   eval(code))
    }}
    

        
    class testIdBool extends TestCase("testIdBool"){ 
      override def runTest() ={
        println("================\n"+name+"\n")
      val x = Name("x")
      val varx:LTerm = Var(x)
      val binding = x\\varx
      val idBoolAST = Lam(TyBool(), binding)
      val code = "\\x:bool.x"
      val idparsed = parseString(code) getOrElse( exit)
      val idparsconv = textualtoAST(idparsed)
      assertEquals("desugar doesn't work properly", idBoolAST, idparsconv) 
      val idtype = typeOf(idBoolAST)
      assertEquals("id is not TyBool:"+idtype, TyArr(TyBool(),TyBool()),idtype)
      val idapplied = App(idBoolAST,Tru())
      assertEquals("ERROR: type of id bool is wrong", TyBool(), typeOf (idapplied))
      val idappliedwrong = App(idBoolAST, Lit(1))
      try {typeOf (idappliedwrong)
        fail("did not detect typing error")}
      catch {
        case e: TypeExc => () //println("OK: detected typing error")
      }
      assertEquals("ERROR: eval not working for id bool",Tru() ,eval(idapplied))
      eval(code)
      
    }}
    

class testIdInt extends TestCase("testIdInt"){ 
  override def runTest() ={
    println("================\n"+name+"\n")
      val x = Name("x")
      val idIntAST = Lam(TyInt(), x\\Var(x))
      val code = "\\x:int.x"
      val idparsed = parseString(code) getOrElse( exit)
      val idparsconv = textualtoAST(idparsed)
      assertEquals("desugar doesn't work properly", idIntAST, idparsconv) 
      if (!(idIntAST equals idparsconv)) println("desugar doesn't work properly")
      val idtype = typeOf (idIntAST);
      assertEquals("id is not TyInt():"+idtype, TyArr(TyInt(),TyInt()),idtype)

      val idapplied = App(idIntAST,Lit(4))
      assertEquals("ERROR: type of id 4 is wrong", TyInt(), typeOf (idapplied))
      val idappliedwrong = App(idIntAST, Tru())
      try {typeOf (idappliedwrong)
        fail("did not detect typing error")}
      catch {
        case e: TypeExc => () //println("OK: detected typing error")
      }
      if (!(eval(idapplied) equals Lit(4)))
        println("ERROR: eval not working for id 4") 
      eval(code)
    }}
    
    
class testIfThenElse extends TestCase("testifthenelse"){ 
  override def runTest() ={
  println("================\n"+name+"\n")
      val ifthenAST = If(Fls(),Tru(),Fls()) 
      val code = "if false then true else false"
      val ifthenparsed = parseString(code) getOrElse exit
      if (!(
          prettyPrint(ifthenAST) //.toString_(new Context(Nil))
          equals (prettyPrint(textualtoAST(ifthenparsed)))))//.toString_(new Context(Nil))) ))
        println("ifthen and ifthenparsed differ")
      eval(code)
        
    }}


    class test01kwi extends TestCase("test01kwi"){ 
      override def runTest() ={
      println("================\n"+name+"\n")
      eval("let x = 23 in ( ((\\y:bool z:int . x) (true)) 2)")
    }}
    
    
    class testEx9_2_2_1 extends TestCase("testEx9_2_2_1"){
      override def runTest() ={
      println("================\n"+name+"\n")
      val x = Name("x")
      val ex9_2_2_1AST=App( Lam(TyBool(),x\\Var(x)) , If(Fls(),Tru(),Fls())  )
      val code = "(\\x:bool.x) (if false then true else false)"
      val parsedAST = parseString(code) getOrElse exit
      assertEquals("ERROR: error type in ex9_2_2_1",TyBool(),typeOf(ex9_2_2_1AST))
      assertEquals("ERROR: error eval ex9_2_2_1", Fls(), eval(ex9_2_2_1AST))
      eval(code)
      }}
    
    
    class testInvert extends TestCase("testInvert"){
      override def runTest() ={
      println("================\n"+name+"\n")
      val namex = Name("x")
      val namey = Name("y")
      val notast = Lam(TyBool(),namex\\If(Tru(),Fls(),Tru()))
      val swapnot = notast.swap(namex,namey)
      val appex = App(Tru(),Tru())
      val swapappex = appex.swap(namex,namey)
      val innerappast = Lam(TyArr(TyBool(),TyBool()), namey\\(App(Var(namey),Tru())))
      val swapinnerapppast = innerappast.swap(namex,namey)
      
      val simplevarast = Var(namex)
      val swapsimplevarast = simplevarast.swap(namex,namey)
      val letast = Let(Tru(), namex\\notast)

      val swaplet = letast.swap(namex,namey)
      val code = "let not = (\\x:bool . (if true then false else true)) in ( (\\y: (bool => bool) . (y (true))) not)"
      assertEquals(Fls(),
                   eval(code))
    }}
    
    // is variable capture handled properly?
    class testBinding extends TestCase("testBinding"){
      override def runTest() ={
      println("================\n"+name+"\n")
      val code = "(\\f: (int => int) . \\x: bool. \\y: int. (f y)) (\\x: int . x) (true) (5)" // TODO: improve parser so redundant parens can be omitted 
      val parsedAST = parseString(code) getOrElse exit
      assertEquals(Lit(5),
                   eval(code))
    }}
    
    // test whether computation indeed loops... >:-)
    def testLoopy {
      println("testLoopy")
      val code = "(\\f:(bool => bool) . f f) (\\f:(bool => bool) . f f)" 
      println(eval(parse(code)))
    }

    class testNoSubRecord extends TestCase("testNoSubRecord") {
      override def runTest() ={
        println("================\n"+name+"\n")
        val code = "(\\r:{x:bool} . from r fld x) ({x=true})"
          assertEquals(Tru(),eval(code))
      }
    }
    class testNoSubRecordAndFun extends TestCase("testNoSubRecordAndFun") {
      override def runTest() ={
        println("================\n"+name+"\n")
        val code = "let sub = \\r:{x:bool,y:int} . (if (from r fld x) then {r=1,s=2} else {r=0,s=1}) in"+
          "         (\\f:({x:bool,y:int}=>{r:int,s:int}) . (f {x=true,y=1}))  (sub)"
          assertEquals(eval("{r=1,s=2}"),eval(code))
      }
    }
    
    def testNoSubRecordAndFun {
      val code = "let sub = \\r:{x:bool} . (if (from r fld x) then {r=1,s=2} else {r=0,s=1}) in (\\f:({x:bool,y:int}=>{r:int}) . f ({x=true,y=1}))  (sub)"
      eval(code)
      
    }
    
    
    class testChunkUnwrap extends TestCase("testChunkUnwrap"){
      override def runTest() ={
      println("================\n"+name+"\n")
      val code = "(\\_: unit . 3) (unit)"
      println(eval(code))
    }}
    
    
    

}
